Nuprl Lemma : ma-interface-kinds_wf
11,40
postcript
pdf
A
:Type,
I
:MaInterface(
A
). ma-interface-kinds(
I
)
(Knd List)
latex
Definitions
Type
,
t
T
,
x
:
A
.
B
(
x
)
,
MaInterface(
T
)
,
f
(
x
)
,
t
.2
,
t
.1
,
map(
f
;
as
)
,
Knd
,
type
List
,
concat(
ll
)
,
ma-interface-kinds(
I
)
Lemmas
ma-interface-kinds-aux1
,
concat
wf
,
Knd
wf
,
ma-interface
wf
origin
A:Type, I:MaInterface(A). ma-interface-kinds(I) 
(Knd List) A:Type, I:MaInterface(A). ma-interface-kinds(I) (Knd List) Tx:A. B(x)